Nuprl Lemma : nat_properties
12,41
postcript
pdf
i
:
.
i
0
latex
ProofTree
Definitions
t
T
,
False
,
P
Q
,
A
,
A
B
,
i
j
,
x
:
A
.
B
(
x
)
,
Lemmas
nat
wf
origin
i:
. i 
0
i:. i 0
T
Q
A
B j x:A. B(x)